.editbox {
  margin: 0;
  padding: 2px;
  font-family: Consolas,monospace;
  font-size: 11.5pt;
  color: black;
}
